T:Type, f:(TT), L:(T List), x, y:T.
x=f*(y) via L  (a:T. (a  L)  {x is f*(a) & a is f*(y)}) 

latex

Definitions	t  T, x:AB(x), s = t, Type, , x:A  B(x), y is f*(x), P & Q, {T}, (x  l), P  Q, x:A. B(x), y=f*(x) via L, type List, False, A, Void, a < b, x:A. B(x), , [car / cdr], hd(l), A c B, , left + right, P  Q, P  Q, [], <a, b>, i <z j, i z j, l[i], s ~ t, A  B, , #$n, ||as||, n+m, i  j < k, i  j , {x:A| B(x)} , {i..j}, A List, x.A(x), x,y,z. t(x;y;z), f(a), y = f+(x)
Lemmas	fun-connected weakening, fun-connected transitivity, fun-path-induction, member singleton, select member, nat wf, int seg wf, member wf, non neg length, length wf1, le wf, cons member, fun-connected weakening eq, strict-fun-connected-step, not wf, false wf, fun-connected wf, guard wf, l member wf, fun-path wf